| Definitions | x when e, (x after e),  b, (state when e),  e@i. P(e),  x:A. B(x), state@i, recognizer(es;i;ds;x;k;T;test), i <z j, i  z j, nth_tl(n;as), hd(l), False, A B, i j < k, ||as||, {i..j }, l[i],   b, A c B, A, Knd, {T}, SQType(T), f || g, Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), t.2, t.1, (i = j), p q, R-interface-compat(A;B), R-discrete_compat(A;B), R-frame-compat(A;B), R-base-domain(R), p = q, Rda(R), Rds(R), R-loc(R), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), Y, A || B,  , True,  T, P   Q, P & Q, P  Q, Top, tt, if b then t else f fi ,   x. t(x), DeclaredType(ds;x), ff, t  T, Normal(T), P Q,  , State(ds), x:A. B(x), P  Q, Dec(P), @i(x:T), @i events of kind k change x to f State(ds) (val:T), @i x initially v:T, R-Feasible(R), Unit, x(s), @i only events in L change x : T, R ||- es.P(es), State(ds),  , R-base-recognize(i;ds;x;k;T;test) |
| Lemmas | es-le wf, es-le weakening, es-locl transitivity1, es-pred-locl, es-after-pred2, int-rational, member singleton, l member wf, es-le-iff, false wf, es-dtype wf, es-when-first-discrete, es-when wf, es-le weakening eq, bool sq, es-loc-pred, es-pred wf, es-first wf, decidable equal Kind, es-state-subtype-iff, es-le-loc, es-state-when wf, es-vartype wf, es-after wf, iff wf, alle-at-iff, es-E wf, es-loc wf, es-kind wf, es-val wf, vartype-es-state-sub, recognizer wf, R-base-recognize wf, R-implies-rule, le wf, IdLnk wf, select member, fpf-empty-compatible-left, fpf-compatible-join, R-compat-Rplus-sq, effect-p wf, decl-type wf, Id sq, fpf-single-dom, ma-state-subtype, ifthenelse wf, Reffect wf, Rplus wf, not functionality wrt iff, fpf-empty wf, Kind-deq wf, fpf-empty-compatible-right, fpf-compatible-self, assert-eq-id, eq id wf, frame-p wf, event system wf, init-p wf, Rframe wf, rationals wf, Rinit wf, R-and-rule, fpf wf, Knd wf, decl-state wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, lnk wf, ldst wf, Id wf, isrcv wf, normal-type wf, normal-ds wf, normal-ds-single, normal-ds-join, unit wf, subtype rel self, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, btrue wf, fpf-cap-single-join, true wf, squash wf, member wf, eqtt to assert, fpf-compatible-single2, fpf-sub-join-right, subtype-fpf-cap-top, fpf-cap wf, subtype rel dep function, eqof eq btrue, fpf-single-dom-sq, fpf-cap-single, top wf, fpf-single wf, fpf-join-cap-sq, fpf-single wf3, fpf-join wf, R-effect-rule, bool-inhabited, R-frame-rule, bfalse wf, bool wf, R-init-rule |
Type, x:Id, k:Knd, T:Type, test:(State(ds)